// ApplicationTerm.cpp : implementation file
//
/*#ifndef _APPLICATIONTERM_CPP
#define _APPLICATIONTERM_CPP

#ifdef _STDAFX_H
*/
#include "stdafx.h"
//#endif 

#include "ApplicationTerm.h"
Token::const_reference ApplicationTerm::getRight() const {
	return LeftRight.getRight();
	};


Term::const_reference ApplicationTerm::getLeft() const	 {
	return _TERM(LeftRight.getLeft());
	};

Term::pointer ApplicationTerm::normalized() const{
	
	Term::pointer NewLeft = getLeft().normalized();
	Term::pointer Res = NULL;
	
	if((getRight().isType())&&(NewLeft->isAbstractTypeTerm())){
		Term::pointer Temp = static_cast<Term::pointer>(NewLeft->applyArgument(getRight( )));
		Res = Temp->normalized();
		delete Temp;
	}
	
	if(getRight().isTerm()){
		Term::pointer NewRight = _TERM(getRight()).normalized();
		if(NewLeft->isAbstractTerm()){	
			Term::pointer Temp = static_cast<Term::pointer>(NewLeft->applyArgument(*NewRight));
			Res = Temp->normalized();
			delete Temp;			
			}
		else{
			  Res = new ApplicationTerm(*NewLeft, *NewRight);
			}
			delete NewRight;
		}
				
		
			
	if(!Res) Res = new ApplicationTerm(*NewLeft, getRight( ));

	delete NewLeft;
	return Res;
}

Token::pointer ApplicationTerm::applyArgument(Token::const_reference To)  const{
	return new ApplicationTerm(*this, To);
	}
Token::pointer ApplicationTerm::clone() const{
      return new ApplicationTerm(*this);
}


bool ApplicationTerm::isReducible() const {
	if(isRedex()) return true;
	if(getLeft().isReducible()) return true;
	if(getRight( ).isTerm( ) && _TERM(getRight()).isReducible()) return true;
	return false;
}
bool ApplicationTerm::isRedex() const{
		if(getRight().isTerm())
			return getLeft().isAbstractTerm();
		else
			return getLeft().isAbstractTypeTerm();
}
string ApplicationTerm::toString() const{

		return getLeft().toString() + string("(")
					+ getRight().toString() + string(")");
	
}

string ApplicationTerm::view() const{
	return string("[[")+
		getLeft().view() + string("][") + 
		getRight().view() + string("]]") + 
		string(":")+getType().view();
}

bool ApplicationTerm::operator==(Token::const_reference To)const{
	if(To.isTerm())
		if(_TERM(To).isApplicationTerm())
			return(LeftRight==(_APPLICATIONTERM(To)).LeftRight);

	return false;
}
Token::pointer ApplicationTerm::replaceAll(Token::const_reference To1, Token::const_reference To2) const{
	if((*this)==To1) return To2.clone( );
	Token* NewLeft   = getLeft( ).replaceAll(To1, To2);
	Token* NewRight;
	if(getRight( ).isType( )){
		if(To1.isType( ))
			NewRight = getRight( ).replaceAll(To1, To2);	
		else
			NewRight = getRight( ).clone( );
		}
	else
		NewRight =  getRight( ).replaceAll(To1, To2);	 
	ApplicationTerm* AppPtr = new ApplicationTerm(_TERM(*NewLeft), *NewRight);
	delete NewLeft;
	delete NewRight;
	return AppPtr;
}





bool ApplicationTerm::TypeOccursinFreeVariable(Type::const_reference Ty) const {
	if(getLeft().TypeOccursinFreeVariable(Ty)) return true;
	if(getRight().isTerm()) return _TERM(getRight()).TypeOccursinFreeVariable(Ty);
	return false;
	}







ApplicationTerm::ApplicationTerm(Term::const_reference TL, Token::const_reference TR, const string& ss):
	Term(TL.getType( )), LeftRight(TL,TR)
{
   try{
	   if(TL.getType( ).isAbstractType( ) && !TR.isType( )) throw Term::exception("ApplicationTerm::ApplicationTerm(Term::const_reference, Token::const_reference, const string&)");
	   Token::pointer Ty;
	   
	   if(TR.isType())
		   Ty =  TL.getType( ).applyArgument(_TYPE(TR));
	   else
		   Ty = TL.getType( ).applyArgument( _TERM(TR).getType( ));

	   this->assignType(_TYPE(*Ty));
	   delete Ty;

       }
   catch(Term::exception err){
       throw err;
    }
}

ApplicationTerm::ApplicationTerm(const ApplicationTerm& Ter):
Term(Ter),LeftRight(Ter.LeftRight){}
ApplicationTerm::~ApplicationTerm(){}
const Token* ApplicationTerm::car( ) 	const {return &getLeft( );}
const Token* ApplicationTerm::cdr( ) 	const {return &getRight( );}
const Token* ApplicationTerm::cadr( )	const{
	if(getLeft( ).isApplicationTerm( )) 
		return &(_APPLICATIONTERM(getLeft( )).getRight( ));
	return NULL;
	}

const Token* ApplicationTerm::caar( ) 	const{
	if(getLeft( ).isApplicationTerm( )) 
		return &(_APPLICATIONTERM(getLeft( )).getLeft( ));
	return NULL;
	}



InvertedListTerm::InvertedListTerm(vector<Token*> TV, const string& ss):
	Term(ss), Applications(TV){		
		try{
			Token::pointer Ty = _TERM(*TV[0]).getType( ).clone( );
			for(size_t i =1; i<Applications.size( ); i++){				
				if(Applications[i].isTerm( )){
					Token::pointer Temp = Ty->applyArgument(_TERM(Applications[i]).getType( ));
					delete Ty;
					Ty = Temp;
					}
				else{
					Token::pointer Temp = Ty->applyArgument(Applications[i]);
					delete Ty;
					Ty = Temp;
					}
				}
			this->assignType(_TYPE(*Ty));
			delete Ty;
			return;
			}
		
	catch(Token::exception err){ throw err;}
	}
InvertedListTerm::~InvertedListTerm(){


	}




Token::pointer VirtualInvertedListTerm::toNewTerm(size_t numElts, size_t index) const{
	if(index >= size( )) throw Term::exception("Token::pointer VirtualInvertedListTerm::toNewTerm(size_t index, size_t numElts)"); 
	if(!index && numElts > size( )) throw Term::exception("Token::pointer VirtualInvertedListTerm::toNewTerm(size_t index, size_t numElts) const"); 
	
	if(index){return operator[ ](index).clone( );}
	Token::pointer TPtr = operator[ ](0).clone( );
	for(size_t i=1; i<numElts; i++){
		Token::pointer Temp = TPtr->applyArgument(operator[ ](i));
		delete TPtr;
		TPtr = Temp;
		}
	return TPtr;
	}
Term::pointer VirtualInvertedListTerm::normalized() const{
	Token::pointer Temp = toNewTerm(size( ));
	Term::pointer Res = _TERM(*Temp).normalized( );
	delete Temp;
	return Res;
	}

Token::pointer VirtualInvertedListTerm::applyArgument(Token::const_reference To)  const{
	Token::pointer Temp = toNewTerm(size( ));;
	Token::pointer Res = Temp->applyArgument(To);
	delete Temp;
	return Res;
	}

Token::pointer VirtualInvertedListTerm::clone() const{
	return new VirtualInvertedListTerm(*this);
	}
bool VirtualInvertedListTerm::isReducible() const{
	for(size_t i=0; i<Applications.size( ); i++)
		if(Applications[i]->isTerm( ))
			if(_TERM(*Applications[i]).isReducible( ))
				return true;
	
	if(size( ) > 1)
		return ApplicationTerm(_TERM(*Applications[0]), *Applications[1]).isReducible( );
	return false;
	}


string VirtualInvertedListTerm::toString() const{
	if(hasSyntax( )) return getSyntax( );
	string Res("[");
	for(size_t i=0; i<size( ); i++){
		Res += (operator[ ](i)).toString();
		if(i < size( )-1) Res += string(", ");
	}
	Res += string("]");
	return Res;
	}


string VirtualInvertedListTerm::view() const{
	string Res("[");
	for(size_t i=0; i<size( ); i++){
		Res += (operator[ ](i)).view( );
		if(i < size( )-1) Res += string(", ");
		}
	Res += string("]");
	return Res;
	}

bool VirtualInvertedListTerm::operator==(Token::const_reference To) const{
	if(To.isTerm( ))
		if(_TERM(To).isVirtualInvertedListTerm( ))
			if(_VIRTUALINVERTEDLISTTERM(To).size( ) == size( )){
				for(size_t i = 0; i<size( ); i++)
					if(!(operator[ ](i).operator==(_VIRTUALINVERTEDLISTTERM(To)[i])))
						return false;
				return true;
				}
		return false;
	}

Token::pointer VirtualInvertedListTerm::replaceAll(Token::const_reference To1, Token::const_reference To2) const{
	Token::pointer Temp = toNewTerm(size( ));;
	Token::pointer Res = Temp->replaceAll(To1, To2);
	delete Temp;
	return Res;
	}	
size_t VirtualInvertedListTerm::complexity() const{
	size_t Sum = 0;
	for(size_t i=0; i<size( ); i++)
		Sum += (operator[ ](i)).complexity( );
	return Sum + Term::complexity( );
	}
bool VirtualInvertedListTerm::TypeOccursinFreeVariable(Type::const_reference Ty) const{
	for(size_t i=0; i<size( ); i++)
		if(operator[ ](i).isTerm( ))
			if(_TERM(operator[ ](i)).TypeOccursinFreeVariable(Ty)) return true;

	return false;
	}
Token::const_reference VirtualInvertedListTerm::operator[ ](size_t index) const{
	if(index >= size( )) throw Token::exception("Out of Bound");
	return *Applications[index]; 
	}
const Token* VirtualInvertedListTerm::ptrAtIndex(size_t index) const{
	if(index >= size( )) throw Token::exception("Out of Bound");
	return Applications[index]; 
	}

void VirtualInvertedListTerm::replaceElts(const VirtualInvertedListTerm& VIL, size_t num, size_t index){
	/*Token::pointer TPtr = toNewTerm(num, index);
	
	
	for(size_t i=0; i<index; i++)
	if(index) Applications[i] = 
	if(TPtr->isTerm( )){
			



		}
	if(index == 0){
		= operator[ ](0).clone( );
		for(size_t i=1; i<num; i++){
			Token::pointer Temp = TPtr->applyArgument(operator[ ](i));
			delete TPtr;
			TPtr = Temp;
			}
	if(VIL.getType( ) == _TERM(*TPtr).getType( ))
		}*/
	}
void VirtualInvertedListTerm::push_back(Token::const_reference To){
	if(getType( ).isAbstractType( ) && !To.isType( )) throw Term::exception("void VirtualInvertedListTerm::push_back(Token::const_reference)");
	Token::pointer NewType;
	if(To.isType( ))
		NewType = getType( ).applyArgument(To);
	else
		NewType = getType( ).applyArgument(_TERM(To).getType( ));

	this->assignType(_TYPE(*NewType));
	delete NewType;
	Applications.push_back(&To);
	}

VirtualInvertedListTerm::VirtualInvertedListTerm(Term::const_reference Ter,  const string& ss):
	Term(Ter.getType( ), ss){
	this->Applications.push_back(&Ter);
}


VirtualInvertedListTerm::VirtualInvertedListTerm(const VirtualInvertedListTerm& VIL):Term(VIL){
	Applications.push_back(VIL.Applications[0]);
	for(size_t i=1; i < VIL.size( ); i++)
		push_back(VIL[i]);
}

VirtualInvertedListTerm::~VirtualInvertedListTerm(){}

//#endif











